#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <algorithm>

#include "parser.h"
#include "literal.h"
#include "cnf_data.h"
#include "global.h"

using namespace std;

// the globally available data is defined here.
CNFData* __data;

bool parse_file( char* inFileName )
{
	ifstream inFile ( inFileName );

	if ( !inFile )
	{
		cout << "[parser] Unable to open input file: " << inFileName << endl;
		return false;
	}

	cout << "[parser] Start parsing data." << endl;

	string line = "";
	string str = "";
	int totalVar = 0;
	int totalClause = 0;
	unsigned int lineNumber = 0;
	char nextChar = ' ';

	vector < vector <int> > literalVec;
	vector <Lit> unitClauseVec;
	vector < vector <Lit> > rawClauseVec;
	int value = 0;
	int skippedLine = 0;

	while ( getline( inFile, line ) )
	{
		++lineNumber;
		istringstream iss( line );

		nextChar = iss.peek();
		if ( nextChar == 'c' )
		{ continue; }
		else if ( nextChar == 'p' )
		{
			iss >> str;
			if ( str != "p" )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": need the first \"p\"." << endl;
				return false;
			}

			if ( !(iss >> str) )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": missing the second \"cnf\"." << endl;
				return false;
			}
			else if ( str != "cnf" )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": missing the second \"cnf\"." << endl;
				return false;
			}

			if ( !(iss >> totalVar) )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": missing the total variable count." << endl;
				return false;
			}
			else if ( totalVar < 1 )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": invalid total variable count = " << totalVar << endl;
				return false;
			}

			if ( !(iss >> totalClause) )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": missing the total clause count." << endl;
				return false;
			}
			else if ( totalClause < 1 )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": invalid total clause count = " << totalClause << endl;
				return false;
			}

			cout << "[parser] Input CNF with " << totalVar << " variables and " << totalClause << " clauses." << endl;
		}
		else if ( iss.good() == true )
		{
			vector <Lit> tempClause;

			while ( iss >> value )
			{
				if ( value == 0 )
				{ break; }

				vector <int> tempLit;
				bool sign = (value < 0) ? true : false;
				int varId = abs( value ) - 1;
				Lit lit = Lit( varId, sign );
				size_t id = lit.index();

				if ( id >= literalVec.size() )
				{ literalVec.insert( literalVec.end(), ((((id + 2) >> 1) << 1) - literalVec.size()), tempLit ); }

				tempClause.push_back( lit );
			}

			if ( tempClause.size() == 0 )
			{ cout << "[parser] Empty clause at line #" << lineNumber << ", skipped." << endl; }
			else if ( tempClause.size() == 1 )
			{
				unitClauseVec.push_back( tempClause.front() );
#ifdef DEBUG_PARSER
				cout << "[parser] Clause at line #" << lineNumber << " is added into unit clauses." << endl;
#endif
			}
			else
			{
				bool skip = false;

				for ( vector <Lit>::iterator it1 = tempClause.begin(); it1 != tempClause.end(); ++it1 )
				{
					for ( vector <Lit>::iterator it2 = (it1 + 1); it2 != tempClause.end(); )
					{
						if ( (*it1) == (*it2) )
						{
							cout << "[parser] Line #" << lineNumber << " has duplicated literal #" << it1->index() << " and #" << it2->index() << endl;
							it2 = tempClause.erase(it2);
						}
						else
						{
							if ( (*it1) == ~(*it2) )
							{
								skip = true;
								cout << "[parser] Line #" << lineNumber << " is always true for literal #" << it1->index() << " and #" << it2->index() << endl;
								break;
							}
							++it2;
						}
					}

					if ( skip == true )
					{ break; }
				}

				if ( skip == false )
				{
					if ( tempClause.size() == 0 )
					{ cout << "[parser] Clause at line #" << lineNumber << " is empty after checking, skipped." << endl; }
					else if ( tempClause.size() == 1 )
					{
						unitClauseVec.push_back( tempClause.front() );
#ifdef DEBUG_PARSER
						cout << "[parser] Clause at line #" << lineNumber << " is added into unit clauses after checking." << endl;
#endif
					}
					else
					{
						sort( tempClause.begin(), tempClause.end() );
						rawClauseVec.push_back( tempClause );
					}
				}
				else
				{ ++skippedLine; }
			}

			if ( value != 0 )
			{
				cout << "[parser] Incorrect DIMACS CNF format at line #" << lineNumber << ": missing the last \"0\"." << endl;
				return false;
			}
		}
	}

	// Check data consistency. literalVec is empty now.
	if ( (totalVar << 1) != literalVec.size() )
	{
			cout << "[parser] Warning! The variable count in the first line mismatches the actual input data." << endl;
			cout << (literalVec.size() >> 1) << " variables (" << literalVec.size() << " literals) were read." << endl;
	}
	if ( totalClause != (unitClauseVec.size() + rawClauseVec.size() + skippedLine) )
	{
			cout << "[parser] Warning! The clause count in the first line mismatches the actual input data." << endl;
			cout << (unitClauseVec.size() + rawClauseVec.size() + skippedLine) << " clauses were read." << endl;
	}

	// Sort clauseVec by size.
	vector < vector <size_t> > sizeIndex;

	for ( size_t i = 0; i < rawClauseVec.size(); ++i )
	{
		vector <size_t> tempVec;

		if ( ((rawClauseVec.at(i)).size() + 1) > sizeIndex.size() )
		{ sizeIndex.insert( sizeIndex.end(), ( (rawClauseVec.at(i)).size() + 1 - sizeIndex.size() ), tempVec ); }

		sizeIndex.at((rawClauseVec.at(i)).size()).push_back(i);
	}

	vector <Lit> tempLitVec;
	vector < vector <Lit> > clauseVec;
	clauseVec.reserve( rawClauseVec.size() );

	for ( vector < vector <size_t> >::iterator it1 = sizeIndex.begin(); it1 != sizeIndex.end(); ++it1 )
	{
		for ( vector <size_t>::iterator it2 = (*it1).begin(); it2 != (*it1).end(); ++it2 )
		{
			clauseVec.push_back( rawClauseVec.at(*it2) );
		}
	}

#ifdef DEBUG_PARSER
	// print data for manual check.
	cout << "Sorted raw clauses:" << endl;
	for ( size_t i = 0; i < clauseVec.size(); ++i )
	{
		cout << i << ": ";
		for ( size_t j = 0; j < clauseVec.at(i).size(); ++j )
		{
			cout << (clauseVec.at(i).at(j)).index() << ", ";
		}
		cout << endl;
	}
	cout << endl;
#endif
/*
	// Checking subsumption takes much time.
	// Checking subsumption for unit clauses.
	for ( vector <Lit>::iterator it1 = unitClauseVec.begin(); it1 != unitClauseVec.end(); ++it1 )
	{
		for ( vector <Lit>::iterator it2 = (it1 + 1); it2 != unitClauseVec.end(); )
		{
			if ( (*it1) == ~(*it2) )
			{
				cout << endl << "*** [parser] Input unit clauses indicate this problem is UNSAT. ***" << endl << endl;
				return false;
			}

			if ( (*it1) == (*it2) )
			{ it2 = unitClauseVec.erase(it2); }
			else
			{ ++it2; }
		}

		for ( vector < vector <Lit> >::iterator itVec = clauseVec.begin(); itVec != clauseVec.end(); )
		{
			bool subsumed = false;

			for ( vector <Lit>::iterator it2 = (*itVec).begin(); it2 != (*itVec).end(); ++it2 )
			{
				if ( (*it1) == (*it2) )
				{
					subsumed = true;
					break;
				}
			}

			if ( subsumed == true )
			{ itVec = clauseVec.erase( itVec ); }
			else
			{ ++itVec; }
		}
	}

	vector <bool> clauseEraseMark( clauseVec.size(), false );

	// Temporary literalVec.
	size_t clauseIndex = 0;

	for ( vector < vector <Lit> >::iterator itVec = clauseVec.begin(); itVec != clauseVec.end(); ++itVec )
	{
		for ( vector <Lit>::iterator it = (*itVec).begin(); it != (*itVec).end(); ++it )
		{
			( literalVec.at( index(*it) ) ).push_back( clauseIndex );
		}
		++clauseIndex;
	}

	// Checking subsumption for other clauses.
	for ( size_t i = 0; i < clauseVec.size(); ++i )
	{
		if ( clauseEraseMark.at(i) == true )
		{ continue; }

		vector <int> tempList( (literalVec.at(index((clauseVec.at(i)).front()))).begin(), (literalVec.at(index((clauseVec.at(i)).front()))).end() );

		for ( vector <Lit>::iterator it = ((clauseVec.at(i)).begin() + 1); it != (clauseVec.at(i)).end(); ++it )
		{
			vector <int> intersection( (literalVec.at(index(*it))).size(), 0 );

			vector <int>::iterator it2 = set_intersection( tempList.begin(), tempList.end(),
				(literalVec.at(index(*it))).begin(), (literalVec.at(index(*it))).end(),
				intersection.begin() );

			tempList.assign( intersection.begin(), it2 );
		}

#ifdef DEBUG_PARSER
		cout << "i = " << i << ", tempList: ";
		for ( vector <int>::iterator it = tempList.begin(); it != tempList.end(); ++it )
		{
			cout << (*it) << ", ";
		}
		cout << endl;
#endif
		if ( tempList.size() == 1 )
		{
			if ( i != tempList.front() )
			{ cout << "[parser] Assertion fail: Intersection of clause indices has no original clause." << endl; }
		}
		else if ( tempList.size() > 1 )
		{
			for ( size_t j = 0; j < tempList.size(); ++j )
			{
				if ( j == i )
				{ continue; }

				clauseEraseMark.at(tempList.at(j)) = true;
			}
		}
		else
		{ cout << "[parser] Assertion fail: Intersection of clause indices is empty." << endl; }
	}

	size_t iMark = 0;

	for ( vector < vector <Lit> >::iterator itVec = clauseVec.begin(); itVec != clauseVec.end(); ++iMark )
	{
		if ( clauseEraseMark.at(iMark) == true )
		{ 
			itVec = clauseVec.erase( itVec );
#ifdef DEBUG_PARSER
			cout << "Erasing clauseVec[" << iMark << "]." << endl;
#endif
		}
		else
		{ ++itVec; }
	}

	// Final literalVec.
	// Clear all data in literalVec.
	for ( vector < vector <int> >::iterator itVec = literalVec.begin(); itVec != literalVec.end(); ++itVec )
	{ (*itVec).clear(); }

	clauseIndex = 0;
*/
	size_t clauseIndex = 0;
	// Construct final literalVec.
	for ( vector < vector <Lit> >::iterator itVec = clauseVec.begin(); itVec != clauseVec.end(); ++itVec )
	{
		for ( vector <Lit>::iterator it = (*itVec).begin(); it != (*itVec).end(); ++it )
		{
			( literalVec.at( it->index() ) ).push_back( clauseIndex );
		}
		++clauseIndex;
	}	

	__data = new CNFData();

	__data->_litArrIndexSize = literalVec.size() + 1;
	__data->_claArrIndexSize = clauseVec.size() + 1;

#ifdef DEBUG_PARSER
	cout << "__data->_litArrIndexSize = " << __data->_litArrIndexSize << endl;
	cout << "__data->_claArrIndexSize = " << __data->_claArrIndexSize << endl;
#endif

	__data->_litArrSize = 0;

	// count the total space needed for memory allocation.
	// the empty vectors are skipped.
	for ( size_t i = 0; i < literalVec.size(); ++i )
	{ __data->_litArrSize += literalVec.at(i).size(); }

#ifdef DEBUG_PARSER
	cout << "__data->_litArrSize = " << __data->_litArrSize << endl;
#endif

	__data->_unitClaArrSize = unitClauseVec.size();
	__data->_claArrSize = 0;

	for ( size_t i = 0; i < clauseVec.size(); ++i )
	{ __data->_claArrSize += clauseVec.at(i).size(); }

#ifdef DEBUG_PARSER
	cout << "__data->_unitClaArrSize = " << __data->_unitClaArrSize << endl;
	cout << "__data->_claArrSize = " << __data->_claArrSize << endl;
	cout << endl;
#endif

	// allocate the variable and clause array.
	// Use pinned memory.
	// According to the reference manual, cudaHostAllocDefault = 0.
	__data->allocate_pinned_memory( (void**)&__data->_litArr, __data->_litArrSize * sizeof(int), 0 );
	__data->allocate_pinned_memory( (void**)&__data->_unitClaArr, __data->_unitClaArrSize * sizeof(Lit), 0 );
	__data->allocate_pinned_memory( (void**)&__data->_claArr, __data->_claArrSize * sizeof(Lit), 0 );
	__data->allocate_pinned_memory( (void**)&__data->_litArrIndex, __data->_litArrIndexSize * sizeof(unsigned int), 0 );
	__data->allocate_pinned_memory( (void**)&__data->_claArrIndex, __data->_claArrIndexSize * sizeof(unsigned int), 0 );
	__data->allocate_pinned_memory( (void**)&__data->_varAssignment, (__data->_litArrSize >> 1) * sizeof(Lbool), 0 );

	unsigned int litIndexCount = 0;
	unsigned int claIndexCount = 0;

	for ( int i = 0; i < __data->_unitClaArrSize; ++i )
	{
		__data->_unitClaArr[i] = unitClauseVec.at(i);
	}

	for ( int i = 0; i < (__data->_litArrIndexSize - 1); ++i )
	{
		__data->_litArrIndex[i] = litIndexCount;

		for ( size_t j = 0; j < literalVec.at(i).size(); ++j )
		{
			__data->_litArr[litIndexCount] = literalVec.at(i).at(j);
			++litIndexCount;
		}
	}
	__data->_litArrIndex[__data->_litArrIndexSize - 1] = litIndexCount;

	for ( int i = 0; i < (__data->_claArrIndexSize - 1); ++i )
	{
		__data->_claArrIndex[i] = claIndexCount;

		for ( size_t j = 0; j < clauseVec.at(i).size(); ++j )
		{
			__data->_claArr[claIndexCount] = clauseVec.at(i).at(j);
			++claIndexCount;
		}
	}
	__data->_claArrIndex[__data->_claArrIndexSize - 1] = claIndexCount;

#ifdef DEBUG_PARSER
	// print data for manual check.
	cout << "Literals:" << endl;
	for ( size_t i = 0; i < literalVec.size(); ++i )
	{
		cout << i << ": ";
		for ( size_t j = 0; j < literalVec.at(i).size(); ++j )
		{
			cout << literalVec.at(i).at(j) << ", ";
		}
		cout << endl;
	}
	cout << endl;

	cout << "Unit clauses:" << endl;
	for ( size_t i = 0; i < unitClauseVec.size(); ++i )
	{
		cout << (unitClauseVec.at(i)).index() << ", ";
		cout << endl;
	}
	cout << endl;

	cout << "Clauses:" << endl;
	for ( size_t i = 0; i < clauseVec.size(); ++i )
	{
		cout << i << ": ";
		for ( size_t j = 0; j < clauseVec.at(i).size(); ++j )
		{
			cout << (clauseVec.at(i).at(j)).index() << ", ";
		}
		cout << endl;
	}

	cout << "__data->_litArr:" << endl;
	for ( int i = 0; i < __data->_litArrSize; ++i )
	{
		cout << __data->_litArr[i] << ", ";
		if ( (i % 5) == 9 )
		{ cout << endl; }
	}
	cout << endl;

	cout << "__data->_litArrIndex:" << endl;
	for ( int i = 0; i < __data->_litArrIndexSize; ++i )
	{
		cout << __data->_litArrIndex[i] << ", ";
		if ( (i % 5) == 9 )
		{ cout << endl; }
	}
	cout << endl;

	cout << "__data->_claArr:" << endl;
	for ( int i = 0; i < __data->_claArrSize; ++i )
	{
		cout << (__data->_claArr[i]).index() << ", ";
		if ( (i % 5) == 9 )
		{ cout << endl; }
	}
	cout << endl;

	cout << "__data->_claArrIndex:" << endl;
	for ( int i = 0; i < __data->_claArrIndexSize; ++i )
	{
		cout << __data->_claArrIndex[i] << ", ";
		if ( (i % 5) == 9 )
		{ cout << endl; }
	}
	cout << endl;
#endif

	inFile.close();
	return true;
}

bool write_file( char* outFileName )
{
	ofstream outFile ( outFileName );

	if ( !outFile )
	{
		cout << "[parser] Unable to open output file: " << outFileName << endl;
		return false;
	}

	if ( __data->_output.empty() == false )
	{
		outFile << "SAT" << endl;

		unsigned int i = 0;
		std::vector < std::vector < Lbool > >::const_iterator it1;

		for ( it1 = __data->_output.begin(); it1 != __data->_output.end(); ++it1 )
		{
			outFile << "c Solution #" << i << ":" << endl;
			unsigned int j = 1;
			std::vector < Lbool >::const_iterator it2;
			for ( it2 = (*it1).begin(); it2 != (*it1).end(); ++it2 )
			{
				outFile << (((*it2) == __Lbool_True) ? "" : "-") << j << " ";
				++j;
			}
			outFile << endl;
			++i;
		}
	}
	else
	{ outFile << "UNSAT" << endl; }

	outFile.close();
	return true;
}
